#!/usr/bin/env perl

# Copyright 2014 The Souper Authors. All rights reserved.
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#     http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

use warnings;
use strict;
use Redis;
use Getopt::Long;
use File::Temp;
use Time::HiRes;

eval { require Sys::CPU; Sys::CPU->import(); };
my $NPROCS = 4;
$NPROCS = Sys::CPU::cpu_count() if defined(&Sys::CPU::cpu_count);

my $souper = "@CMAKE_BINARY_DIR@/souper";
my $llvmas = "@LLVM_BINDIR@/llvm-as";
my $llvmopt = "@LLVM_BINDIR@/opt";
my $llvmdis = "@LLVM_BINDIR@/llvm-dis";
my $check = "@CMAKE_BINARY_DIR@/souper-check";
my $triager = "@CMAKE_BINARY_DIR@/py_souper2llvm";

sub runit ($) {
    my $cmd = shift;
    my $res = (system "$cmd");
    return $? >> 8;
}

sub usage() {
    print <<'END';
Options:
  -neg         Infer Neg DFA
  -nonneg      Infer nonNegative DFA
  -nonzero     Infer non Zero DFA
  -power       Infer power of two DFA
  -knownbits   Infer known bits DFA
  -signBits    Infer number of sign bits DFA
END
    exit -1;
}

my $NONNEG = 0;
my $NEG = 0;
my $KNOWNBITS = 0;
my $POWERTWO = 0;
my $NONZERO = 0;
my $SIGNBITS = 0;
my $noopt_count=0;
my %values;
my %sprofiles;
my %dprofiles;
my %sprofile_locs;
my %dprofile_locs;
my %toprint;
my %known;

GetOptions(
    "neg" => \$NEG,
    "nonNeg" => \$NONNEG,
    "nonZero" => \$NONZERO,
    "power" => \$POWERTWO,
    "knownbits" => \$KNOWNBITS,
    "signbits" => \$SIGNBITS,
    ) or usage();

my $r = Redis->new();
$r->ping || die "no server?";
my @all_keys = $r->keys('*');

print "; Inspecting ".scalar(@all_keys)." Redis values\n";

sub souper_known ($) {
    (my $opt) = @_;
    (my $fh, my $tmpfn) = File::Temp::tempfile();
    print $fh $opt;
    $fh->flush();
    my $arg = "";
    if ($NEG) {
        $arg = "-infer-neg -solver-timeout=30";
    } elsif ($NONNEG) {
        $arg = "-infer-non-neg -solver-timeout=30";
    } elsif ($NONZERO) {
        $arg = "-infer-non-zero -solver-timeout=30";
    } elsif ($POWERTWO) {
        $arg = "-infer-power-two -solver-timeout=30";
    } elsif ($KNOWNBITS) {
        $arg = "-infer-known-bits -solver-timeout=30";
    } elsif ($SIGNBITS) {
        $arg = "-infer-sign-bits -solver-timeout=30";
    }
    my $cmd = "${check} $arg < $tmpfn 2>/dev/null |";
    open INF, $cmd;
    my $k = "";
    while (my $line = <INF>) {
        chomp $line;
        if ($NEG) {
            if ($line =~ /negative from souper: (.*)$/) {
                $k = $1;
            }
        } elsif ($NONNEG) {
            if ($line =~ /nonNegative from souper: (.*)$/) {
                $k = $1;
            }
        } elsif ($NONZERO) {
            if ($line =~ /nonZero from souper: (.*)$/) {
                $k = $1;
            }
        } elsif ($POWERTWO) {
            if ($line =~ /powerOfTwo from souper: (.*)$/) {
                $k = $1;
            }
        } elsif ($KNOWNBITS) {
            if ($line =~ /knownBits from souper: (.*)$/) {
                $k = $1;
            }
        } elsif ($SIGNBITS) {
            if ($line =~ /signBits from souper: (.*)$/) {
                $k = $1;
            }
        }
    }
    close INF;
    close $fh;
    unlink $tmpfn;
    print $opt if not defined $k;
    return $k;
}

sub add_sprofile($$) {
    (my $opt, my $href) = @_;
    my %h = %{$href};
    foreach my $k (keys %h) {
        $sprofile_locs{$opt}{$k} += $h{$k};
    }
    if (!$sprofile_locs{$opt}) {
        $sprofile_locs{$opt} = {};
    }
}

sub add_dprofile($$) {
    (my $opt, my $href) = @_;
    my %h = %{$href};
    foreach my $k (keys %h) {
        $dprofile_locs{$opt}{$k} += $h{$k};
    }
    if (!$dprofile_locs{$opt}) {
        $dprofile_locs{$opt} = {};
    }
}

my $xcnt = 0;
foreach my $opt (@all_keys) {
    my %h = $r->hgetall($opt);
    my $result = $h{"result"};
    my $known = $h{"known"};
    my $sprofile = 0;
    my $dprofile = 0;
    my %sprofile_loc;
    my %dprofile_loc;
    foreach my $kk (keys %h) {
        if ($kk =~ /^sprofile (.*)$/) {
            my $count = $h{$kk};
            $sprofile += $count;
            $sprofile_loc{$1} += $count;
        }
        if ($kk =~ /^dprofile (.*)$/) {
            my $count = $h{$kk};
            $dprofile += $count;
            $dprofile_loc{$1} += $count;
        }
    }
    if (defined $result) {
        $opt .= $result;
        if ($result eq "") {
            $noopt_count++;
        }
    }
    $known{$opt} = $known;
    $toprint{$opt} = 1;
    add_sprofile($opt, \%sprofile_loc);
    add_dprofile($opt, \%dprofile_loc);
    $sprofiles{$opt} = $sprofile;
    $dprofiles{$opt} = $dprofile;
}

sub replace($$) {
    (my $old, my $new) = @_;
    die if $new eq "";
    $sprofiles{$new} += $sprofiles{$old};
    $dprofiles{$new} += $dprofiles{$old};
    my %ss = %{$sprofile_locs{$old}};
    add_sprofile($new, \%ss);
    my %dd = %{$dprofile_locs{$old}};
    add_dprofile($new, \%dd);
    $toprint{$new} = 1;
    delete $toprint{$old};
}

sub remove($) {
    (my $opt) = @_;
    delete $toprint{$opt};
    delete $sprofiles{$opt};
    delete $dprofiles{$opt};
    delete $sprofile_locs{$opt};
    delete $dprofile_locs{$opt};
}

my $status_cnt;
my $status_opct;
my $status_total;

sub reset_status($) {
    (my $t) = @_;
    $status_total = $t;
    $status_opct = 0;
    $status_cnt = 0;
}

sub status() {
    print ".";
    $status_cnt++;
    my $pct = int(100.0*$status_cnt/$status_total);
    if ($pct > $status_opct) {
        $status_opct = $pct;
        print "$pct %\n";
    }
}

sub total_profile_count() {
    my $cnt = 0;
    foreach my $opt (keys %toprint) {
        $cnt += $sprofiles{$opt} + $dprofiles{$opt};
    }
    return $cnt;
}

if (0) {
    my @keys = keys %toprint;
    foreach my $opt (@keys) {
        my $newopt = $opt;
        $newopt =~ s/ \(.*\)//gm;
        if ($opt ne $newopt) {
            replace($opt, $newopt);
        }
    }
}

sub llvm_known($) {
    (my $opt) = @_;
    (my $fh1, my $fn1) = File::Temp::tempfile();
    print $fh1 $opt;
    close $fh1;
    if ($NEG) {
        open INF, "$triager < $fn1 | $llvmas | $souper -print-neg-at-return |" or die;
    } elsif ($NONNEG) {
        open INF, "$triager < $fn1 | $llvmas | $souper -print-nonneg-at-return |" or die;
    } elsif ($NONZERO) {
        open INF, "$triager < $fn1 | $llvmas | $souper -print-non-zero-at-return |" or die;
    } elsif ($POWERTWO) {
        open INF, "$triager < $fn1 | $llvmas | $souper -print-power-two-at-return |" or die;
    } elsif ($KNOWNBITS) {
        open INF, "$triager < $fn1 | $llvmas | $souper -print-known-at-return |" or die;
    } elsif ($SIGNBITS) {
        open INF, "$triager < $fn1 | $llvmas | $souper -print-sign-bits-at-return |" or die;
    }
    my $known;
    while (my $line = <INF>) {
        chomp $line;
        if ($NEG) {
            if ($line =~ /negative from compiler: (.*)$/) {
                $known = $1;
            }
        } elsif ($NONNEG) {
            if ($line =~ /nonNegative from compiler: (.*)$/) {
                $known = $1;
            }
        } elsif ($NONZERO) {
            if ($line =~ /nonZero from compiler: (.*)$/) {
                $known = $1;
            }
        } elsif ($POWERTWO) {
            if ($line =~ /powerOfTwo from compiler: (.*)$/) {
                $known = $1;
            }
        } elsif ($KNOWNBITS) {
            if ($line =~ /known bits from compiler: (.*)$/) {
                $known = $1;
            }
        } elsif ($SIGNBITS) {
            if ($line =~ /signBits from compiler: (.*)$/) {
                $known = $1;
            }
        }
    }
    close INF;
    print $opt if not defined $k;
    return $known if defined $known;
    return "oops";
}

sub bylen { length $a <=> length $b }
sub bysprofile { $sprofiles{$b} <=> $sprofiles{$a} }
sub bydprofile { $dprofiles{$b} <=> $dprofiles{$a} }

print "\n\n";

sub compare_facts($$) {
    my $res = "";
    my $llvm_stronger = 0;
    my $souper_stronger = 0;
    my $souper_timeout = 0;
    my ($sk, $lk) = (@_);
    if ($sk eq "") {
        $souper_timeout = 1;
    }
    if ($lk eq "") {
        die "Compiler didn't compute the fact";
    }
    if ($NEG || $NONNEG ||$POWERTWO || $NONZERO) {
        if ($sk eq "true") {
            $souper_stronger = 1;
        }
        if ($lk eq "true") {
            $llvm_stronger = 1;
        }
    } elsif ($KNOWNBITS) {
        if (length($lk) == length($sk)) {
            for (my $i=0; $i<length($lk); $i++) {
                if ((substr($sk,$i,1) eq "x") && (substr($lk,$i,1) ne "x")) {
                     $llvm_stronger = 1;
                }
                if ((substr($lk,$i,1) eq "x") && (substr($sk,$i,1) ne "x")) {
                     $souper_stronger = 1;
                }
            }
        } else {
          if ($souper_timeout == 0) {
              die "length of knownBits computed by Souper and LLVM mismatch";
          }
        }
    } elsif ($SIGNBITS) {
        if ($sk > $lk) {
            $souper_stronger = 1;
        }
        if ($lk > $sk) {
            $llvm_stronger = 1;
        }
        if ($sk == $lk) {
            $souper_stronger = 1;
            $llvm_stronger = 1;
        }
    }

    if ($souper_timeout) {
        $res .= "; timeout: Souper didn't compute the dataflow fact";
    } elsif ($llvm_stronger && $souper_stronger) {
        $res .= "; neither is stronger";
    } elsif ($llvm_stronger) {
        $res .= "; llvm is stronger";
    } elsif ($souper_stronger) {
        $res .= "; souper is stronger";
    } else {
        die;
    }
    $res .= "\n";
    return $res;
}

sub go($$) {
    (my $opt, my $counter) = @_;
    print "LHS Counter = $counter\n";
    my $ret = "";
    $ret .= "$opt";
    $ret .= "\n";

    my $sk = souper_known($opt);
    $ret .= "; known from Souper:   $sk\n";

    my $lk;
    if (0) {
        $lk = $known{$opt};
        if (!defined($lk)) {
            if ($SIGNBITS) {
                $lk = "0";
            } else {
                $lk = "";
                if ($KNOWNBITS) {
                    for (my $i=0; $i<length($sk); $i++) {
                        $lk .= "x";
                    }
                }
            }
        }
    } else {
        $lk = llvm_known($opt);
    }
    $ret .= "; known from compiler: $lk\n";

    my $print = 0;
    if ($sk ne $lk) {
        $print = 1;
        $ret .= compare_facts($sk, $lk);
    }
    $ret .= "\n";
    $ret .= "; total static profile = $sprofiles{$opt}\n";
    $ret .= "; total dynamic profile = $dprofiles{$opt}\n";
    $ret .= "------------------------------------------------------\n\n";
    if ($print) {
        my $fname ='';
        if ($NEG) {
            $fname = 'neg_' . sprintf("%08d", $counter);
        } elsif ($NONNEG) {
            $fname = 'nonneg_' . sprintf("%08d", $counter);
        } elsif ($NONZERO) {
            $fname = 'nonzero_' . sprintf("%08d", $counter);
        } elsif ($KNOWNBITS) {
            $fname = 'knownbits_' . sprintf("%08d", $counter);
        } elsif ($POWERTWO) {
            $fname = 'power_' . sprintf("%08d", $counter);
        } elsif ($SIGNBITS) {
            $fname = 'signbits_' . sprintf("%08d", $counter);
        } else {
            die "dataflow option not specified";
        }
        open(my $fh, '>', $fname);
        print $fh $ret;
        close $fh;
    }
    exit();
}

my $num_running = 0;
my $opid = $$;

sub wait_for_one() {
    my $xpid = wait();
    die if $xpid == -1;
    $num_running--;
}

my $counter=0;
foreach my $opt (sort bysprofile keys %toprint) {
    $counter++;
    wait_for_one() unless $num_running < $NPROCS;
    die unless $num_running < $NPROCS;
    my $pid = fork();
    die unless $pid >= 0;
    go($opt, $counter) if $pid == 0;
    # make sure we're in the parent
    die unless $$ == $opid;
    $num_running++;
}

wait_for_one() while $num_running > 0;

print "\n\nDone.\n";
